Iof proof for Lemma dec iff ex bvfun:
1. T : Type
2. E : T
T
3. f : T
T
4.
x, y:T. (
(f(x,y))) 
(E(x,y))
5. x : T
6. y : T
Dec((f(x,y)))
by (Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)
.| 12,41 |
T
T
x, y:T. ((f(x,y))) (E(x,y))
Dec((f(x,y)))
by (Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)
.
| Definitions |  Tx:A. B(x) |
| Lemmas |